1
2
3
4 package trace;
5
6 import java.util.Enumeration;
7 import java.util.HashMap;
8 import java.util.Iterator;
9 import java.util.LinkedList;
10 import java.util.Vector;
11 import java.util.zip.GZIPInputStream;
12 import java.io.FileInputStream;
13 import java.io.IOException;
14 import java.io.InputStream;
15 import java.io.PrintStream;
16 import net.sf.javabdd.BDD;
17 import net.sf.javabdd.BDDFactory;
18 import net.sf.javabdd.BDDPairing;
19
20 /***
21 * A driver to run BDD trace files in the bwolen BDD trace format.
22 * See http://www-2.cs.cmu.edu/~bwolen/software/.
23 *
24 * This code is based on the code in JDD.
25 *
26 * @author jwhaley
27 * @version $Id: TraceDriver.java 469 2006-11-29 08:07:31Z joewhaley $
28 */
29 public class TraceDriver {
30
31 static PrintStream out = System.out;
32
33
34 class TracedVariable {
35 public String name;
36 public int index, last_use;
37 BDD bdd;
38 public boolean is_var = false;
39 public void showName() {
40 out.print(name);
41 }
42 public void show() {
43 out.print("\n\t");
44 showName();
45 out.println();
46 bdd.printSet();
47 }
48 }
49
50
51 abstract class TracedOperation {
52 public int index, size = -1;
53 public String op;
54 public void show() { }
55 public abstract void execute() throws IOException ;
56 public void show_code() { }
57 }
58
59
60 class TracedDebugOperation extends TracedOperation {
61 public String text;
62 public void execute() {
63 if (verbose
64 out.println(text);
65 }
66 public void show_code() { out.println( "//" + text); }
67 }
68
69 class TracedSaveOperation extends TracedOperation {
70 public TracedVariable v;
71 public void execute() {
72 try {
73 bdd.save(v.name + ".buddy", v.bdd);
74
75 } catch(IOException exx) {
76
77 }
78 }
79 public void show_code() {
80 out.println("BDDIO.saveBuDDy(bdd, " + v.bdd + ",\"" + v.name + ".buddy\");");
81 }
82 }
83
84 class TracedPrintOperation extends TracedOperation {
85 public TracedVariable v;
86 public boolean graph;
87 public void execute() {
88 if(graph) v.bdd.printDot();
89 else { out.println(v.name + ":"); v.bdd.printSet(); }
90 }
91 public void show_code() {
92 if(graph) out.println(v.name + ".printDot();");
93 else out.println(v.name + ".printSet();");
94 }
95 }
96
97 class TracedCheckOperation extends TracedOperation {
98 public TracedVariable t1,t2;
99 public void execute() throws IOException {
100 boolean equal = (t1.bdd.equals(t2.bdd));
101 if(size != -1) {
102 boolean expected = (size == 0 ? false : true);
103 if(equal != expected)
104 throw new IOException ("are_equal(" + t1.name + ", " + t2.name + ") failed. expected " + expected + ", got " + equal);
105 }
106 }
107 public void show() {
108 out.print(index + "\t");
109 out.print("are_equal("+t1.name+", "+t2.name+");");
110 if(size != -1) out.print("\t% " + size);
111 out.println();
112 }
113 }
114
115 class TracedReorderOperation extends TracedOperation {
116 public BDDFactory.ReorderMethod method;
117 public void execute() throws IOException {
118 bdd.reorder(method);
119 }
120 public void show() {
121 out.print(index + "\t");
122 out.print("reorder("+method+");");
123 out.println();
124 }
125 }
126
127
128 class TracedBDDOperation extends TracedOperation {
129 public int ops;
130 public TracedVariable ret, op1, op2, op3;
131 public Vector operands;
132
133 public void show() {
134 out.print(index + "\t");
135 ret.showName();
136 out.print(" = ");
137
138 if(op.equals("=") ) {
139 op1.showName();
140 out.print(";");
141 } else {
142 out.print(op + "(" );
143 boolean first = true;
144 for (Enumeration e = operands.elements() ; e.hasMoreElements() ;) {
145 TracedVariable v = (TracedVariable)e.nextElement();
146 if(first) first = false; else out.print(", ");
147 v.showName();
148 }
149 out.print(");");
150 }
151
152 if(size != -1) out.print("\t% " + size);
153 out.println();
154 }
155
156 public void execute() throws IOException {
157
158
159 ret.bdd.free();
160
161 if(op.equals("not")) do_not();
162 else if(op.equals("=")) do_assign();
163 else if(op.equals("and")) do_and();
164 else if(op.equals("or")) do_or();
165 else if(op.equals("xor")) do_xor();
166 else if(op.equals("xnor")) do_xnor();
167 else if(op.equals("nor")) do_nor();
168 else if(op.equals("nand")) do_nand();
169 else if(op.equals("ite")) do_ite();
170 else if(op.equals("vars_curr_to_next")) do_s2sp();
171 else if(op.equals("vars_next_to_curr")) do_sp2s();
172 else if(op.equals("support_vars")) do_support();
173 else if(op.equals("exists")) do_exists();
174 else if(op.equals("forall")) do_forall();
175 else if(op.equals("restrict")) do_restrict();
176 else if(op.equals("rel_prod")) do_relprod();
177 else {
178 throw new IOException("Unknown operation '" + op + "', #" + op_count );
179 }
180
181 last_assignment = ret;
182
183 if(size != -1) {
184 int size2 = node_count(ret);
185 if(size != size2) {
186 out.println("\n*************************************************************************");
187 out.println("Size comparison failed after " + op + " ( wanted " + size + ", got " + size2 + ")");
188 show();
189 out.println("\n");
190 throw new IOException("Size comparison failed");
191
192 }
193 }
194
195 checkVar(this);
196 }
197
198
199 private void do_not() throws IOException {
200 checkEquality(ops, 1, "do_not");
201 ret.bdd = op1.bdd.not();
202 }
203
204
205 private void do_assign() throws IOException {
206 checkEquality(ops, 1, "do_assign");
207 ret.bdd = op1.bdd;
208 }
209
210 private void do_or() {
211 if(ops == 2) ret.bdd = op1.bdd.or(op2.bdd);
212 else {
213 for (Enumeration e = operands.elements() ; e.hasMoreElements() ;)
214 if(((TracedVariable)e.nextElement()).bdd.isUniverse()) { ret.bdd = bdd.universe(); return; }
215
216 BDD tmp = bdd.zero();
217 for (Enumeration e = operands.elements() ; e.hasMoreElements() ;) {
218 TracedVariable v = (TracedVariable)e.nextElement();
219 BDD tmp2 = tmp.or(v.bdd);
220 tmp.free(); tmp = tmp2;
221 }
222 ret.bdd = tmp;
223 }
224
225 }
226
227 private void do_and() {
228 if(ops == 2) ret.bdd = op1.bdd.and(op2.bdd);
229 else {
230 for (Enumeration e = operands.elements() ; e.hasMoreElements() ;)
231 if(((TracedVariable)e.nextElement()).bdd.isZero()) { ret.bdd = bdd.zero(); return; }
232
233 BDD tmp = bdd.universe();
234 for (Enumeration e = operands.elements() ; e.hasMoreElements() ;) {
235 TracedVariable v = (TracedVariable)e.nextElement();
236 BDD tmp2 = tmp.and(v.bdd);
237 tmp.free(); tmp = tmp2;
238 }
239 ret.bdd = tmp;
240 }
241 }
242
243 private void do_nand() {
244 if(ops == 2) ret.bdd = op1.bdd.apply(op2.bdd, BDDFactory.nand);
245 else {
246 do_and();
247 BDD tmp = ret.bdd;
248 ret.bdd = tmp.not();
249 tmp.free();
250 }
251 }
252
253 private void do_nor() {
254 if(ops == 2) ret.bdd = op1.bdd.apply(op2.bdd, BDDFactory.nor);
255 else {
256 do_or();
257 BDD tmp = ret.bdd;
258 ret.bdd = tmp.not();
259 tmp.free();
260 }
261
262 }
263
264
265 private void do_xor() throws IOException { check(ops == 2); ret.bdd = op1.bdd.xor(op2.bdd); }
266 private void do_xnor() throws IOException { check(ops == 2); ret.bdd = op1.bdd.biimp(op2.bdd); }
267
268 private void do_ite() throws IOException { check(ops == 3); ret.bdd = op1.bdd.ite(op2.bdd, op3.bdd); }
269 private void do_s2sp() throws IOException { check(ops == 1); ret.bdd = op1.bdd.replace(s2sp); }
270 private void do_sp2s() throws IOException { check(ops == 1); ret.bdd = op1.bdd.replace(sp2s); }
271
272 private void do_support() throws IOException { check(ops == 1); ret.bdd = op1.bdd.support().toBDD(); }
273 private void do_exists() throws IOException { check(ops == 2); ret.bdd = op2.bdd.exist(op1.bdd.toVarSet()); }
274
275 private void do_forall() throws IOException { check(ops == 2); ret.bdd = op2.bdd.forAll(op1.bdd.toVarSet()); }
276 private void do_restrict() throws IOException { check(ops == 2); ret.bdd = op1.bdd.restrict(op2.bdd); }
277 private void do_relprod() throws IOException { check(ops == 3); ret.bdd = op2.bdd.relprod(op3.bdd, op1.bdd.toVarSet()); }
278
279
280
281
282
283 public void show_code() {
284 String code;
285 Enumeration e = operands.elements();
286 TracedVariable v = (TracedVariable)e.nextElement();
287 if(op.equals("=")) out.println("BDD " + ret.name + " = " + v.name + ";");
288 else {
289 out.print("BDD " + ret.name + " = " +v.name + "." +op);
290 out.print("(");
291 boolean mode2 = op.equals("ite");
292 int i = 0;
293 for (i = 0; e.hasMoreElements() ;i++) {
294 v = (TracedVariable)e.nextElement();
295 if(mode2 && i != 0) out.print(", ");
296 out.print(v.name);
297
298 if(e.hasMoreElements() && !mode2) out.print( "." + op + "(");
299
300 }
301 if(!mode2) for(int j = 1; j < i; j++) out.print(")");
302
303 out.println(");");
304 }
305
306 if(op.equals("ite") )
307 out.println("System.out.println(\"" + ret.name + " ==> \"+" + ret.name + ".nodeCount());" );
308 }
309
310 }
311
312
313 private static final int DEFAULT_NODES = 500000, MAX_NODES = 3000000;
314 private BDDFactory bdd;
315 private InputStream is;
316 private StringBuffer sb;
317 private String filename, module;
318 private int [] stack;
319 private int stack_tos, nodes, cache, vars;
320 private static int auto_reorder = Integer.parseInt(System.getProperty("reorder", "0"));
321 private HashMap map;
322 private BDDPairing s2sp, sp2s;
323 private TracedVariable last_assignment;
324 private Vector operations, variables;
325 private int op_count, line_count, var_count;
326 private long time;
327
328 /*** this is our extra VERBOSE flags, to enable trace_verbose_print() output*/
329 public static boolean verbose = false;
330
331 public TraceDriver(String file) throws IOException
332 {
333 this(file, DEFAULT_NODES);
334 }
335
336 public TraceDriver(String file, int nodes) throws IOException
337 {
338 this(file,
339 file.endsWith(".gz") ?
340 (InputStream) new GZIPInputStream(new FileInputStream(file)) :
341 (InputStream) new FileInputStream(file),
342 nodes);
343 }
344
345
346 public TraceDriver(String file, InputStream is) throws IOException
347 {
348 this(file, is, DEFAULT_NODES);
349 }
350
351
352 public TraceDriver(String file, InputStream is, int nodes) throws IOException {
353 this.filename = file;
354 this.nodes = nodes;
355 this.is = is;
356 this.sb = new StringBuffer();
357 this.stack = new int[64];
358 this.stack_tos = 0;
359 this.cache = Math.max( Math.min(nodes / 10, 5000), 50000);
360 this.map = new HashMap(1024);
361
362 this.operations = new Vector();
363 this.variables = new Vector();
364 this.op_count = 0;
365 this.line_count = 1;
366 this.var_count = 0;
367
368
369
370 TracedVariable vret = new TracedVariable();
371 vret.last_use = 0;
372 vret.name = "0";
373
374 map.put("0", vret);
375
376 vret = new TracedVariable();
377 vret.last_use = 0;
378 vret.name = "1";
379
380 map.put("1", vret);
381
382 last_assignment = null;
383
384
385 parse();
386
387
388 vret = (TracedVariable) map.get("0");
389 vret.bdd = bdd.zero();
390 vret = (TracedVariable) map.get("1");
391 vret.bdd = bdd.one();
392
393 execute();
394
395 show_results();
396 bdd.done();
397
398 }
399
400
401 private void show_code() {
402 out.println("import org.sf.javabdd.*;\n"+
403 "public class Test {\n"+
404 "public static void main(String[] args) {\n");
405
406 out.println("\n\n" +
407 "BDDFactory B = BDDFactory.init("+nodes+",100);\n" +
408 "B.setVarNum(" + variables.size() + ");\nBDD ");
409
410 int i = 0;
411 for (Enumeration e = variables.elements() ; e.hasMoreElements() ;) {
412 TracedVariable v = (TracedVariable)e.nextElement();
413 if(v.is_var) {
414 if(i != 0) out.print(",");
415 out.print(v.name + "=B.ithVar(" + i+ ") ");
416 i++;
417 }
418 }
419 out.println(";");
420
421 for (Enumeration e = operations.elements() ; e.hasMoreElements() ;) {
422 TracedOperation v = (TracedOperation)e.nextElement();
423 v.show_code();
424 }
425
426 out.println("}\n}\n");
427 }
428
429 private void setup_bdd(int vars) {
430 this.vars = vars;
431
432
433 out.println();
434 out.println("loading " + module + " from " + filename + " (" + nodes + " nodes, " + vars + " vars)");
435
436 bdd = BDDFactory.init(nodes, cache);
437 if (auto_reorder != 0) {
438 out.println("setting auto reorder to " + auto_reorder);
439 bdd.autoReorder(getReorderMethod(auto_reorder));
440 try {
441 java.lang.reflect.Method cb = TraceDriver.class.getDeclaredMethod("reorder_callback", new Class[] { boolean.class, BDDFactory.ReorderStats.class });
442 bdd.registerReorderCallback(this, cb);
443 } catch (NoSuchMethodException x) {
444 System.out.println("Cannot find callback method");
445 }
446 }
447
448 }
449
450 public static void reorder_callback(boolean prestate, BDDFactory.ReorderStats s) {
451 System.out.print(prestate?"Start":"Finish");
452 System.out.println("ing reorder.");
453 if (!prestate) System.out.println(s);
454 }
455
456
457 private void alloc_var(String name) {
458 TracedVariable vret = new TracedVariable();
459 vret.last_use = 0;
460 int vn = bdd.extVarNum(1);
461 vret.bdd = bdd.ithVar(vn);
462 vret.name = name;
463 vret.is_var = true;
464 map.put(name, vret);
465 variables.add(vret);
466 var_count++;
467 }
468
469 private void checkVar(TracedBDDOperation tp) {
470 checkVar(tp.ret);
471 for (Enumeration e = tp.operands.elements() ; e.hasMoreElements() ;) {
472 TracedVariable v = (TracedVariable)e.nextElement();
473 checkVar(v);
474 }
475 }
476
477 private void checkVar(TracedVariable v) {
478 if(v != null && v.last_use == op_count) {
479
480 v.bdd.free();
481 v.last_use = -1;
482
483 }
484 }
485
486 private TracedPrintOperation createPrintOperation(boolean graph, TracedVariable v) {
487 TracedPrintOperation tp = new TracedPrintOperation();
488 tp.index = op_count;
489 tp.graph = graph;
490 tp.v = v;
491 operations.add( tp );
492 return tp;
493 }
494
495 private TracedSaveOperation createSaveOperation(TracedVariable v) {
496 TracedSaveOperation ts = new TracedSaveOperation();
497 ts.index = op_count;
498 ts.v = v;
499 operations.add( ts );
500 return ts;
501 }
502 private TracedCheckOperation createCheckOperation(TracedVariable v1, TracedVariable v2) {
503 TracedCheckOperation tp = new TracedCheckOperation();
504 tp.index = op_count;
505 tp.t1 = v1;
506 tp.t2 = v2;
507 operations.add( tp );
508 return tp;
509 }
510 private TracedDebugOperation createDebugOperation(String text) {
511 TracedDebugOperation tp = new TracedDebugOperation();
512 tp.index = op_count;
513 tp.text = text;
514 operations.add( tp );
515 return tp;
516 }
517 private TracedBDDOperation createBDDOperation() {
518 TracedBDDOperation tp = new TracedBDDOperation();
519 tp.index = op_count;
520 operations.add( tp );
521 tp.operands = new Vector(3);
522 return tp;
523 }
524 private TracedReorderOperation createReorderOperation(BDDFactory.ReorderMethod m) {
525 TracedReorderOperation tp = new TracedReorderOperation();
526 tp.index = op_count;
527 tp.method = m;
528 operations.add(tp);
529 return tp;
530 }
531
532
533
534
535 private void show_results() {
536 time = System.currentTimeMillis() - time;
537 out.println("" + op_count + " operations performed, total execution time: " + time + " [ms]");
538
539
540
541 if(verbose) {
542 if(false && last_assignment != null && last_assignment.hashCode() != -1) {
543 int size = node_count(last_assignment);
544 out.println("Last assignment: " + last_assignment.name + ", " + size + " nodes.");
545
546 out.println("\n");
547 }
548 out.println("Nodes: "+bdd.getNodeNum()+"/"+bdd.getNodeTableSize());
549 out.println(bdd.getGCStats());
550 bdd.printStat();
551 }
552
553 if (auto_reorder != 0) {
554 out.println("Final variable order:");
555 bdd.printOrder();
556 }
557 }
558
559 /*** check if the variables to be used are OK */
560 private void check_all_variables() {
561 for (Enumeration e = variables.elements() ; e.hasMoreElements() ;) {
562 TracedVariable v = (TracedVariable)e.nextElement();
563 if(v.last_use >= op_count) {
564
565
566 }
567 }
568 }
569
570
571 private void execute() throws IOException {
572 time = System.currentTimeMillis();
573 for (Enumeration e = operations.elements() ; e.hasMoreElements() ;) {
574 TracedOperation tp = (TracedOperation)e.nextElement();
575 op_count = tp.index;
576
577 if(TraceDriver.verbose) tp.show();
578 tp.execute();
579 }
580 }
581
582 /*** BDD trace driver doesn't count nodes the same way as we do ... */
583 private int node_count(TracedVariable v) {
584 if (v.bdd.hashCode() == -1) throw new InternalError();
585 int size = v.bdd.nodeCount();
586
587 if (v.bdd.isOne() || v.bdd.isZero()) size += 1;
588 else size += 2;
589 return size;
590 }
591
592 private void parse() throws IOException {
593 read_module();
594 read_input();
595 skip_output();
596 read_structure();
597 }
598 private void read_module() throws IOException {
599 need("MODULE");
600 module = need();
601 }
602
603 private void skip_output() throws IOException {
604 need("OUTPUT");
605 for(String tmp = need(); !tmp.equals(";"); tmp = need()) ;
606 }
607
608 private void read_structure() throws IOException {
609 need("STRUCTURE");
610 while(true) {
611 String ret = need();
612 if(ret.equals("ENDMODULE")) return;
613
614 op_count++;
615
616
617 if(ret.equals("trace_verbose_print")) {
618 need("("); String str = getString(); need(")"); need(";");
619 createDebugOperation(str);
620 } else if(ret.equals("are_equal")) {
621 need("("); String str = need(); TracedVariable t1 = needVar(str);
622 need(","); str = need(); TracedVariable t2 = needVar(str); need(")"); need(";");
623 createCheckOperation(t1,t2);
624 } else if(ret.equals("print_bdd") || ret.equals("show_bdd") ) {
625 need("("); String str = need(); TracedVariable v = needVar(str);need(")"); need(";");
626 createPrintOperation(ret.equals("show_bdd"), v);
627 } else if(ret.equals("save_bdd")) {
628 need("("); String str = need(); TracedVariable v = needVar(str);need(")"); need(";");
629 createSaveOperation(v);
630 } else if(ret.equals("check_point_for_force_reordering")) {
631 need("("); String str = need();
632 int type = Integer.parseInt(str);
633 need(")"); need(";");
634 BDDFactory.ReorderMethod m = getReorderMethod(type);
635 createReorderOperation(m);
636 } else {
637
638
639 TracedVariable vret = (TracedVariable) map.get(ret);
640 if(vret == null)
641 vret = addTemporaryVariable(ret);
642
643
644
645 need("=");
646 String op = need();
647
648
649 updateUsage(vret);
650
651
652 TracedBDDOperation tp = createBDDOperation();
653 TracedVariable var = (TracedVariable) map.get(op);
654
655 if(var != null) {
656 need(";"); tp.operands.add(var);
657 tp.ret = vret;
658 tp.op = "=";
659 updateUsage(var);
660 } else {
661 tp.op = op;
662 tp.ret = vret;
663 if(op.equals("new_int_leaf")) {
664 need("("); String c = need(); need(")"); need(";");
665 Object operand = map.get(c);
666 if (operand == null) throw new InternalError();
667 tp.operands.add(operand);
668 tp.ret = vret;
669 tp.op = "=";
670 } else {
671 String s1,s2;
672 need("(");
673
674 do {
675 s1 = need();
676 tp.operands.add( needVar(s1) );
677 s1 = need();
678 } while(s1.equals(",") );
679 need(";");
680 }
681 }
682
683 tp.ops = tp.operands.size();
684 if(tp.ops > 0) tp.op1 = (TracedVariable) tp.operands.elementAt(0);
685 if(tp.ops > 1) tp.op2 = (TracedVariable) tp.operands.elementAt(1);
686 if(tp.ops > 2) tp.op3 = (TracedVariable) tp.operands.elementAt(2);
687 }
688 }
689 }
690
691 private static BDDFactory.ReorderMethod getReorderMethod(int type) {
692 BDDFactory.ReorderMethod m;
693 switch (type) {
694 case 0: m = BDDFactory.REORDER_NONE; break;
695 case 1: m = BDDFactory.REORDER_WIN2; break;
696 case 2: m = BDDFactory.REORDER_WIN2ITE; break;
697 case 3: m = BDDFactory.REORDER_WIN3; break;
698 case 4: m = BDDFactory.REORDER_WIN3ITE; break;
699 case 5: m = BDDFactory.REORDER_SIFT; break;
700 case 6: m = BDDFactory.REORDER_SIFTITE; break;
701 case 7: m = BDDFactory.REORDER_RANDOM; break;
702 default: m = BDDFactory.REORDER_NONE; break;
703 }
704 return m;
705 }
706
707
708
709
710 private void read_input() throws IOException {
711 boolean interleave = false;
712 LinkedList list = new LinkedList();
713
714
715 need("INPUT");
716
717 for(int i = 0; ; i++) {
718 String name = need();
719 if(i == 0 && ( name.equals("CURR_NEXT_ASSOCIATE_EVEN_ODD_INPUT_VARS") || name.equals("STATE_VAR_ASSOCIATE_CURR_NEXT_INTERLEAVE"))) {
720 if(name.equals("STATE_VAR_ASSOCIATE_CURR_NEXT_INTERLEAVE")) interleave = true;
721 } else {
722
723 list.add(name);
724
725 name = need();
726 if(name.equals(";")) break;
727 else if(!name.equals(",")) {
728 throw new IOException("expected ',' when reading inputs, but got: " + name+ " at line " + line_count);
729 }
730 }
731 }
732
733 int count = list.size();
734 setup_bdd(count);
735 for(Iterator it = list.iterator(); it.hasNext() ;) {
736 String name = (String) it.next();
737 alloc_var(name);
738 }
739
740
741 int size = variables.size();
742
743 int [] v1 = new int[size /2];
744 int [] v2 = new int[size /2];
745
746 Enumeration e =variables.elements();
747 for (int i = 0; i < (size & ~1) ;i ++) {
748 TracedVariable v = (TracedVariable) e.nextElement();
749 if (v.bdd.nodeCount() > 1) throw new InternalError();
750 if(interleave) {
751 if( (i%2) == 0) v1[i/2] = v.bdd.var();
752 else v2[i/2] = v.bdd.var();
753 } else {
754 if(i < v1.length) v1[i] = v.bdd.var();
755 else v2[ i - v1.length] = v.bdd.var();
756 }
757 }
758
759 s2sp = bdd.makePair();
760 s2sp.set(v1, v2);
761 sp2s = bdd.makePair();
762 sp2s.set(v2, v1);
763
764 bdd.varBlockAll();
765
766
767
768
769 }
770
771 private TracedVariable needVar(String str) throws IOException {
772 TracedVariable ret = (TracedVariable) map.get(str);
773 if(ret == null ) {
774 throw new IOException("Unknown variable/operand " + str + " at line " + line_count);
775 }
776 updateUsage(ret);
777 return ret;
778 }
779
780 private void updateUsage(TracedVariable v) {
781
782 v.last_use = op_count;
783 }
784
785 private TracedVariable addTemporaryVariable(String name) {
786 TracedVariable vret = new TracedVariable();
787 vret.last_use = op_count;
788 vret.name = name;
789 vret.bdd = bdd.zero();
790 variables.add( vret);
791 map.put(name, vret);
792
793 return vret;
794 }
795
796
797 private void need(String what) throws IOException {
798 String got = need();
799 if(!got.equals(what)) {
800 check(false, "Syntax error: expected '" + what + "', but read '" + got + "', op=" + op_count);
801 }
802 }
803
804 private String need() throws IOException {
805 String ret = next();
806 if(ret == null) {
807 check(false, "pre-mature end of file");
808 }
809 return ret;
810 }
811
812 private int read() {
813 int c = -1;
814 if(stack_tos > 0) c = stack[--stack_tos];
815 else {
816 try { c = is.read(); } catch(IOException exx) { }
817 }
818 if(c == '\n') line_count++;
819 return c;
820 }
821
822 private void push(int c) {
823 stack[stack_tos++] = c;
824 if(c == '\n') line_count--;
825 }
826 private boolean isSpace(int c) { return (c == ' ' || c == '\n' || c == '\t' || c == '\r'); }
827 private boolean isAlnum(int c) { return ((c >= '0' && c <= '9') || (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || c == '_' || c == '-'); }
828
829
830
831 private String getString() throws IOException {
832 StringBuffer buffer = new StringBuffer();
833 int c = 0;
834 while( isSpace( c = read()));
835 if(c != '"') throw new IOException("Not an string at line " + line_count);
836
837 while( ( c = read()) != '"')
838 buffer.append((char)c);
839
840 return buffer.toString();
841
842 }
843 private void skip_eol() {
844 for(;;) {
845 int c = read();
846 if(c == -1 || c == '\n') return;
847 }
848 }
849 private String next() {
850 sb.setLength(0);
851 int c;
852 do {
853 c = read();
854 if(c == -1) return null;
855 } while( isSpace(c));
856
857 if(isAlnum(c)) {
858 do {
859 sb.append((char)c);
860 c = read();
861
862 if(c == -1) return sb.toString();
863 } while( isAlnum(c));
864
865 if(!isSpace(c)) push(c);
866 } else {
867 if(c == '%' || c == '#') {
868 int old_line = line_count;
869 if(c == '%') {
870 String count = next();
871 TracedOperation tp = (TracedOperation) operations.lastElement();
872 if(tp.size == -1) tp.size = Integer.parseInt(count);
873 }
874
875 if(old_line == line_count) skip_eol();
876 return next();
877 }
878 return ""+((char)c);
879 }
880
881
882 return sb.toString();
883 }
884
885
886 /package-summary.html">*/ void checkEquality(int a, int b, String txt) throws IOException {
887 if(a != b) throw new IOException(txt + ", " + a + " != " + b);
888 }
889
890 /package-summary.html">*/ void check(boolean b, String txt) throws IOException {
891 if(!b) throw new IOException(txt);
892 }
893
894 /package-summary.html">*/ void check(boolean b) throws IOException {
895 if(!b) throw new IOException("Check failed");
896 }
897
898
899
900 public static void main(String [] args) {
901
902
903 if (args.length == 0) {
904 out.println("Usage: java "+TraceDriver.class.getName()+" file.trace {file2.trace ...}");
905 return;
906 }
907 int bddnodes = Integer.parseInt(System.getProperty("bddnodes", Integer.toString(DEFAULT_NODES)));
908 long totalTime = 0;
909 try {
910 for (int i = 0; i < args.length; ++i) {
911 TraceDriver td = new TraceDriver(args[i], bddnodes);
912 totalTime += td.time;
913 }
914 if (args.length > 1) {
915 out.println("Total time for all traces: "+totalTime+" [ms]");
916 }
917 } catch (IOException exx) {
918 out.println("FAILED: " + exx.getMessage() );
919 exx.printStackTrace();
920 }
921 }
922 }